$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$a$:Knd fp$\rightarrow$ Type. @$i$: with declarations ds:${\it ds}$ da:${\it da}$ $\in$ Dsys